$\forall$$A$:Type, $B$:($A$$\rightarrow$Type), $f$:fpf($A$; $x$.$B$($x$)). ($\uparrow$fpf{-}is{-}empty($f$)) $\Leftarrow\!\Rightarrow$ ($f$ = fpf{-}empty)